﻿using System;
using System.Collections.Generic;
using System.ComponentModel;
using System.Data;
using System.Drawing;
using System.Linq;
using System.Text;
using System.Windows.Forms;

using System.Threading;

using TruthTree2.FOL.Input;
using TruthTree2.FOL.Logic;
using TruthTree2.FOL.Resolution;
using TruthTree2.FOL.ResolutionExtensions;
using TruthTree2.FOL.Proofs;
using TruthTree2.FOL.ProofExtensions;

namespace TruthTree2
{
    internal partial class Form1 : Form
    {
        public Form1()
        {
            InitializeComponent();
        }

        private void stuff()
        {
            Variable x = new Variable("x");
            Variable y = new Variable("y");
            Variable z = new Variable("z");
            WFF sentence;

            // These should be switched to parsing for better readability

            //sentence = new Conjunction(
            //    new Identity(new Constant("a"), new Constant("b")),
            //    new Negation(new Identity(new Constant("b"), new Constant("a"))));

            //sentence = new Negation(
            //     new Biconditional(
            //         new Universal(x,
            //             new Universal(y,
            //                 new Conditional(
            //                     new Predicate("R", x, y),
            //                     new Negation(new Predicate("R", y, x))))),
            //         new Conjunction(
            //             new Universal(x,
            //                 new Universal(y,
            //                     new Conditional(
            //                         new Conjunction(
            //                             new Predicate("R", x, y),
            //                             new Predicate("R", y, x)),
            //                         new Identity(x, y)))),
            //             new Universal(x,
            //                 new Negation(new Predicate("R", x, x))))));

            //sentence = new Conjunction(
            //    new Universal(x,
            //        new Conditional(
            //            new Predicate("P", x),
            //            new Predicate("Q", x))),
            //    new Predicate("P", new Constant("a")),
            //    new Identity(new Constant("a"), new Constant("b")),
            //    new Identity(new Constant("c"), new Constant("b")),
            //    new Negation(new Predicate("Q", new Constant("c"))));

            sentence = new Conjunction(
                new Universal(x,
                    new Conditional(
                        new Predicate("P", x),
                        new Predicate("Q", x))),
                new Universal(x, new Predicate("P", x)),
                new Negation(new Universal(y, new Predicate("Q", y))));

            //sentence = new Conjunction(
            //    new Universal(x,
            //        new Identity(
            //            new Function("+", x, new Constant("0")),
            //            x)),
            //    new Universal(x,
            //        new Identity(
            //            new Function("*", x, new Constant("0")),
            //            new Constant("0"))),
            //    new Universal(x,
            //        new Universal(y,
            //            new Identity(
            //                new Function("*", x, new Function("s", y)),
            //                new Function("+", new Function("*", x, y), x)))),
            //    new Identity(
            //        new Function("*", new Constant("0"), new Constant("0")),
            //        new Constant("0")),
            //    new Negation(
            //        new Universal(x,
            //            new Identity(
            //                new Function("*", new Constant("0"), x),
            //                new Constant("0")))));

            //sentence = new Conjunction(
            //    new Universal(x,
            //        new Identity(
            //            new Function("+", x, new Constant("0")),
            //            x)),
            //    new Universal(x,
            //        new Universal(y,
            //            new Identity(
            //                new Function("+", x, new Function("s", y)),
            //                new Function("s", new Function("+", x, y))))),
            //    new Negation(
            //        new Universal(x,
            //            new Universal(y,
            //                new Universal(z,
            //                    new Identity(
            //                        new Function("+", new Function("+", x, y), z),
            //                        new Function("+", x, new Function("+", y, z))))))));

            //sentence = new Conjunction(
            //    new Universal(x,
            //        new Negation(
            //            new Identity(
            //                new Function("s", x),
            //                new Constant("0")))),
            //    new Universal(x,
            //        new Universal(y,
            //            new Identity(
            //                new Function("+", x, new Function("s", y)),
            //                new Function("s", new Function("+", x, y))))),
            //    new Universal(x,
            //        new Universal(y,
            //            new Biconditional(
            //                new Predicate("<", x, y),
            //                new Existential(z,
            //                    new Identity(
            //                        new Function("+", x, new Function("s", z)),
            //                        y))))),
            //    new Negation(
            //        new Universal(x,
            //            new Negation(new Predicate("<", x, new Constant("0"))))));

            label1.Text = sentence.ToString();

            WFF cnf = sentence.ConvertToCNF();
            label2.Text = cnf.ToString();

            Set res = Set.ToResolutionSet(sentence);
            label3.Text = res.ToString();

            bool valid = res.Resolution();
            label4.Text = "Valid: " + valid.ToString();
        }

        private void button1_Click(object sender, EventArgs e)
        {
            // Resolution is currently not functional
            //stuff();
        }

        private void stuff2()
        {
            Variable x = new Variable("x");
            Variable y = new Variable("y");
            Variable z = new Variable("z");
            List<WFF> sentences = new List<WFF>();

            //sentences.Add(Parser.parseString("(or A B)"));
            //sentences.Add(Parser.parseString("(not (if (not B) D))"));
            //sentences.Add(Parser.parseString("(not A)")); // Conclusion

            //sentences.Add(Parser.parseString("(iff A B)"));
            //sentences.Add(Parser.parseString("(not (or B (not A)))")); // Conclusion

            //sentences.Add(Parser.parseString("(if A B)"));
            //sentences.Add(Parser.parseString("(if B A)"));
            //sentences.Add(Parser.parseString("(not (iff A B))")); // Conclusion

            //sentences.Add(Parser.parseString("(iff A B)"));
            //sentences.Add(Parser.parseString("A"));
            //sentences.Add(Parser.parseString("(not B)")); // Conclusion

            //sentences.Add(Parser.parseString("(forall _x (Big _x))"));
            //sentences.Add(Parser.parseString("(not (Big a))")); // Conclusion

            //sentences.Add(Parser.parseString("(forall _x (forall _y (Magic _x _y)))"));
            //sentences.Add(Parser.parseString("(not (Magic a b))")); // Conclusion

            //sentences.Add(Parser.parseString("(forall _x (forall _y (Magic _x _y)))"));
            //sentences.Add(Parser.parseString("(not (exists _x (forall _y (Magic _x _y))))")); // Conclusion

            //sentences.Add(Parser.parseString("(forall _x (if (P _x) (Q _x)))"));
            //sentences.Add(Parser.parseString("(forall _y (P _y))"));
            //sentences.Add(Parser.parseString("(not (forall _z (Q _z)))")); // Conclusion

            sentences.Add(Parser.parseString("(forall _x (if (P _x) (Q _x)))"));
            sentences.Add(Parser.parseString("(P a)"));
            sentences.Add(Parser.parseString("(= a b)"));
            sentences.Add(Parser.parseString("(= c b)"));
            sentences.Add(Parser.parseString("(not (Q c))")); // Conclusion

            // This one takes longer than I was willing to let it sit. I assume it will out of memory eventually.
            //sentences.Add(Parser.parseString("(forall _x (not (= (s _x) zero)))"));
            //sentences.Add(Parser.parseString("(forall _x (forall _y (= (plus _x (s _y)) (s (plus _x _y)))))"));
            //sentences.Add(Parser.parseString("(forall _x (forall _y (iff (lt _x _y) (exists _z (= (plus _x (s _z)) _y)))))"));
            //sentences.Add(Parser.parseString("(not (forall _x (not (lt _x zero))))")); // Conclusion

            Tree tree = new Tree(sentences);
            tree.Satisfy(30);
            //tree.Clean();

            Bitmap bmptree = new Bitmap(10, 10, System.Drawing.Imaging.PixelFormat.Format24bppRgb);
            Graphics gtree = Graphics.FromImage(bmptree);
            SizeF tsize = tree.ImageSize(gtree);
            bmptree = new Bitmap((int)Math.Ceiling(tsize.Width), (int)Math.Ceiling(tsize.Height), System.Drawing.Imaging.PixelFormat.Format24bppRgb);
            gtree = Graphics.FromImage(bmptree);
            gtree.SmoothingMode = System.Drawing.Drawing2D.SmoothingMode.AntiAlias;
            gtree.TextRenderingHint = System.Drawing.Text.TextRenderingHint.ClearTypeGridFit;
            gtree.Clear(Color.White);
            tree.Draw(gtree);
            bmptree.Save("tree.png");

            label1.Text = "State: " + tree.State;
            label2.Text = "Height: " + tree.Height;
            label3.Text = "Width: " + tree.Width;

            if (tree.State != TreeState.Closed) { return; }

            Subproof proof = new Subproof(sentences);
            proof.FirstLineNumber = 1;
            proof.AddTree(tree);
            proof.Clean();

            SizeF psize = proof.ImageSize(gtree);
            Bitmap bmpproof = new Bitmap((int)Math.Ceiling(psize.Width), (int)Math.Ceiling(psize.Height), System.Drawing.Imaging.PixelFormat.Format24bppRgb);
            Graphics gproof = Graphics.FromImage(bmpproof);
            gproof.TextRenderingHint = System.Drawing.Text.TextRenderingHint.ClearTypeGridFit;
            gproof.Clear(Color.White);
            proof.Draw(gproof);
            bmpproof.Save("proof.png");

            
            label4.Text = "Proof Length: " + (proof.LastLineNumber - 1);
        }

        private void button2_Click(object sender, EventArgs e)
        {
            stuff2();
        }

        private void stuff3()
        {
            label1.Text = "A => " + Parser.parseString("A");
            label2.Text = "(if A B) => " + Parser.parseString("(if A B)");
            label3.Text = "(and A B C D) => " + Parser.parseString("(and A B C D)");
            label4.Text = "(forall _x (exists _y (= (plus _x (s _y)) (s (plus _x _y))))) => " + Parser.parseString("(forall _x (exists _y (= (plus _x (s _y)) (s (plus _x _y)))))");
        }

        private void button3_Click(object sender, EventArgs e)
        {
            stuff3();
        }

        private Thread worker;
        private void button4_Click(object sender, EventArgs e)
        {
            if (worker != null && worker.IsAlive)
            {
                worker.Abort();
                Console.WriteLine("Cancel");
            }
            else
            {
                worker = new Thread(() =>
                {
                    Console.WriteLine("Start");

                    List<WFF> sentences = new List<WFF>();
                    sentences.Add(Parser.parseString("(forall _x (not (= (s _x) zero)))"));
                    sentences.Add(Parser.parseString("(forall _x (forall _y (= (plus _x (s _y)) (s (plus _x _y)))))"));
                    sentences.Add(Parser.parseString("(forall _x (forall _y (iff (lt _x _y) (exists _z (= (plus _x (s _z)) _y)))))"));
                    sentences.Add(Parser.parseString("(not (forall _x (not (lt _x zero))))")); // Conclusion

                    Tree workerTree = new Tree(sentences);
                    workerTree.Satisfy();

                    Console.WriteLine("Done");

                    Bitmap bmptree = new Bitmap(10, 10, System.Drawing.Imaging.PixelFormat.Format24bppRgb);
                    Graphics gtree = Graphics.FromImage(bmptree);
                    SizeF tsize = workerTree.ImageSize(gtree);
                    bmptree = new Bitmap((int)Math.Ceiling(tsize.Width), (int)Math.Ceiling(tsize.Height), System.Drawing.Imaging.PixelFormat.Format24bppRgb);
                    gtree = Graphics.FromImage(bmptree);
                    gtree.SmoothingMode = System.Drawing.Drawing2D.SmoothingMode.AntiAlias;
                    gtree.TextRenderingHint = System.Drawing.Text.TextRenderingHint.ClearTypeGridFit;
                    gtree.Clear(Color.White);
                    workerTree.Draw(gtree);
                    bmptree.Save("tree.png");
                });

                worker.Start();
            }
        }

        private void Form1_FormClosing(object sender, FormClosingEventArgs e)
        {
            if (worker != null && worker.IsAlive) { worker.Abort(); }
        }

        private void Form1_Load(object sender, EventArgs e)
        {

        }
    }
}
